k:Knd. islocal(k)   

latex

Definitions	Knd, islocal(k), b, isl(x), x:A. B(x), IdLnk, t  T, Id
Lemmas	Id wf, IdLnk wf, isl wf, bnot wf